> -- | Dieses Modul implementiert die Mark 1 - Maschine mit IO und Threads

> module CHF.AbsM.CMark1 
> where
> import CHF.AbsM.Heap
> import CHF.Parse.Parser
> import qualified Data.Map as Map
> import qualified CHF.AbsM.Mark1 as M1
> import qualified CHF.AbsM.IOMark1 as IOM1
> import CHF.AbsM.Stack
> import CHF.AbsM.Stack.StackElem
> import CHF.AbsM.Stack.IOStackElem
> import CHF.CoreL.MachineLanguage
> import CHF.CoreL.Language
> import CHF.Transformation.Core2Machine 
> import CHF.SemAna.TypeCheck
> import Data.List
> import Data.Maybe
> import Data.Char 
> import System.Random
> import Debug.Trace

> data CMark1Thread = CMark1Thread {
>      name :: Mark1Var,
>      control :: Mark1Expr, 
>      stack :: (Stack (StackElem Mark1Var [MCAlt Mark1Cons Mark1Var])),
>      ioStack :: Stack (IOStackElem Mark1Var)
>     }

> data CMark1State = CMark1State {
>      heap :: Heap Mark1Var Mark1Expr,
>      mvars :: Heap Mark1Var (Maybe Mark1Var),
>      threads :: Heap Mark1Var CMark1Thread,
>      queue :: [(Int,Mark1Var)]
>   }


> instance Show CMark1State where
>  show m =
>   "Heap:\t" ++ unlines (map show ( Map.assocs  (heap m))) ++
>   "\nMVARS:" ++ unlines (map show ( Map.assocs (mvars m))) ++
>   "\nThreads:" ++ unlines (map show ( Map.assocs (threads m))) ++
>   "\nqueue:" ++  show (queue m) 

> instance Show CMark1Thread where
>  show m =
>   "\nName:\t" ++ show (name m) ++
>   "\nControl:\t" ++ show (control m) ++
>   "\nStack:\t" ++ show (stack m) ++
>   "\nIOStack:\t" ++ show (ioStack m)  


> --------------------------------------------------------------------------------------------------------------------------------------------
> -- | 'startState' berechnet den Startzustand der CMark1
> --------------------------------------------------------------------------------------------------------------------------------------------
> startState :: Mark1Expr -> CMark1State
> startState m1e = let thread = CMark1Thread {name = "_main_",control = m1e, stack = emptyStack, ioStack = emptyStack}
>                  in CMark1State {heap = emptyHeap, mvars = emptyHeap, threads = insertHeap "_main_" thread emptyHeap,queue = [(1,"_main_")]}


> --------------------------------------------------------------------------------------------------------------------------------------------
> -- | 'finalState' berechnet den Endzustand der CMark1
> --------------------------------------------------------------------------------------------------------------------------------------------
> finalState :: CMark1State -> [Mark1Var] -> [Int] -> (CMark1State, [Mark1Var],[Int])
> finalState cm1st m1vars intl =
>   let (cm1st',m1var',intl') = nextState cm1st m1vars intl
>   in case  lookupHeap "_main_" (threads cm1st) of
>			Just (thr,otherthrs)  -> 
> 					if ((isVal (control thr)) && (isEmptyStack (stack thr) && isEmptyStack (ioStack thr))) then  (cm1st,m1vars,intl)
>      				else if isIOVal (control thr) && isEmptyStack (stack thr) && isEmptyStack (ioStack thr) then (cm1st,m1vars,intl)
>		                 --else if ((IOM1.isVar (control thr)) && (isEmptyStack (stack thr)) && (isEmptyStack (stack thr))) then  
>				  			--	case lookupHeap (IOM1.getVar (control thr)) (mvars cm1st) of
>								--		(Just (Just z,mv')) -> (cm1st,m1vars,intl)
>									--	(Just (Nothing,mv')) -> (cm1st,m1vars,intl)
>										--Nothing ->  finalState cm1st' m1var' intl'
>   	                 else finalState cm1st' m1var' intl'



> --------------------------------------------------------------------------------------------------------------------------------------------
> -- | 'nextStateState' berechnet den Folgezustand von CMark1
> --------------------------------------------------------------------------------------------------------------------------------------------
> nextState :: CMark1State -> [Mark1Var] -> [Int] -> (CMark1State, [Mark1Var],[Int])
> nextState  (CMark1State{heap= h, mvars = mv,  threads = t, queue= ((n,x):q)}) (v:vs) (i:is) =
>  case  x of
>   "_main_" ->  case lookupHeap x t of
>						Just (thr,otherthrs) -> 
>								case (control thr) of 
>										(ConsM (Left Fork)   [y]) -> -- fork
>											case isEmptyStack (stack thr) of
>													False -> liftIOM (CMark1State{heap= h, mvars = mv,  threads = t, queue= ((n,x):q)}) thr otherthrs (v:vs) (i:is)
>													True -> fork (CMark1State{heap= h, mvars = mv,  threads = t, queue= ((n,x):q)}) (v:vs) (i:is) thr otherthrs y
>										_ -> liftIOM (CMark1State{heap= h, mvars = mv,  threads = t, queue= ((n,x):q)}) thr otherthrs (v:vs) (i:is)
>						_ -> error "CMark1-Fehler 1"
>   _ -> case lookupHeap x t of
>              Just (thr,otherthrs) -> 
>     	         case isEmptyStack (stack thr) of
>						True -> case isEmptyStack (ioStack thr) of
>										True ->  case (control thr) of
>														(ConsM (Left Return) [y]) -> --unIO
>																(CMark1State{heap= insertHeap x (VarM y) h, mvars = mv ,threads = otherthrs, queue= q},(v:vs),(i:is)) --unIO
>														(ConsM (Left Fork)   [y]) -> fork (CMark1State{heap= h, mvars = mv,  threads = t, queue= ((n,x):q)}) (v:vs) (i:is) thr otherthrs y -- fork
>														_ -> liftIOM (CMark1State{heap= h, mvars = mv,  threads = t, queue= ((n,x):q)}) thr otherthrs (v:vs) (i:is)
>										False -> case (control thr) of
>													(ConsM (Left Fork)   [y]) -> fork (CMark1State{heap= h, mvars = mv,  threads = t, queue= ((n,x):q)}) (v:vs) (i:is) thr otherthrs y -- fork
>													_ -> liftIOM (CMark1State{heap= h, mvars = mv,  threads = t, queue= ((n,x):q)}) thr otherthrs (v:vs) (i:is)
>						_ -> liftIOM (CMark1State{heap= h, mvars = mv,  threads = t, queue= ((n,x):q)}) thr otherthrs (v:vs) (i:is)

> fork (CMark1State{heap= h, mvars = mv,  threads = t, queue= ((n,x):q)}) (v:vs) (i:is) thr otherthrs y=
>  case (n>1) of 
>		True -> (CMark1State{heap= h, mvars = mv ,
>   		 				threads = insertHeap v (CMark1Thread {name = v, control = (VarM y), stack = emptyStack, ioStack = (emptyStack)})
>       										   				  (insertHeap x (CMark1Thread {name = x, 
>       			               				   				  							   control= ConsM (Left Return) [v],
>                                 				   				  							   stack = emptyStack, 
>                                  				   				  							   ioStack = (ioStack thr)}) otherthrs), 
>                   							   				  queue= ((n-1,x): (q ++ [(i,v)]))},vs,is)
>		False -> case (n==1) of
>				True -> (CMark1State{heap= h, mvars = mv ,
>                                    threads = insertHeap v (CMark1Thread {name = v, control = (VarM y), stack = emptyStack, ioStack = (emptyStack)})
>                                                                          (insertHeap x (CMark1Thread {name = x, 
>                                                                                                       control= ConsM (Left Return) [v],
>                                                                                                       stack = emptyStack, 
>                                                                                                       ioStack = (ioStack thr)}) otherthrs), 
>                                                                          queue= ((q ++ [(i,v),(head is,x)]))},vs,tail is)
>				False -> error "CMark1-Fehler 2" 

>
> --------------------------------------------------------------------------------------------------------------------------------------------
> -- | 'liftIOM' liftet die Regeln der IOMark 1 fuer die Concurrent Mark1. Fuer den ausgewaehlten Threat wird eine IO-Mark1-Transition angewendet
> --------------------------------------------------------------------------------------------------------------------------------------------
> liftIOM (CMark1State{heap= h, mvars = mv,  threads = t, queue= ((n,x):q)})  thr otherthrs (v:vs) (i:is)=
>  let 
>      iom1st = (IOM1.IOMark1State {IOM1.heap = h, IOM1.mvars= mv, IOM1.control= (control thr), IOM1.stack = (stack thr), IOM1.ioStack = (ioStack thr)})
>      (iom1st', rvs) = IOM1.nextState iom1st (v:vs)
>  in (setSchedule (CMark1State{heap= (IOM1.heap iom1st'), mvars = (IOM1.mvars iom1st'),  threads = insertHeap x (CMark1Thread {name = x, control= (IOM1.control iom1st'),stack = (IOM1.stack iom1st'), ioStack = (IOM1.ioStack iom1st')}) otherthrs, queue=((n,x):q)}) i,(rvs),(is))

				 


----------------------------------------------------------------------------------------------------------------------------------------------------
===============================================[ Hier folgen nur noch EXEC und die Tests ]==========================================================


> varnamen = ["_y" ++ show i | i <- [1..]]
> zahlen = repeat 1
> zzahlen :: Int -> [Int]
> zzahlen i = randomRs (1,10) (mkStdGen i) 
> testStartState i = startState i
> testNextState i = let (zustand,namen,_) = nextState (testStartState i) varnamen zahlen
>                   in zustand

> testFinaleState i = let (zustand,namen,_) = finalState (testStartState i) varnamen zahlen
>                     in zustand


> test20States i = let s0 = testStartState i
>                  in putStrLn $ unlines $ intersperse "\n" $ map show $ take 80 $ go s0 varnamen zahlen
>  where go s n z = let (s',n',z') = nextState s n z
>                   in s:(go s' n' z')

> testExec i j = exec i varnamen (zzahlen j)

> testFinaleState' i j = let (zustand,namen,_) = finalState (testStartState i) varnamen (zzahlen j)
>                        in zustand

> test20States' i j = let s0 = testStartState i
>                  in writeFile "test.out" $ unlines $ intersperse "\n" $ map show $ take 800 $ go s0 varnamen (zahlen)
>  where go s n z = let (s',n',z') = nextState s n z
>                   in s:(go s' n' z')

------------------------

> t1    = toMachineExpr "expression \\x -> x"
> t1'  =  toMachineExpr "expression \\x -> x"
>       --    LamM "_x1" (VarM "_x1")

> t2  =  toMachineExpr "data Bool = True | False expression letrec x=True in case x of {False -> True}"
>          -- LetrecM ["_x1" := ConsM (Right "True") []] (CaseM (VarM "_x1") [CAltM "False" [] (ConsM (Right "True") [])])

> t3  =  toMachineExpr "data Bool = True | False expression letrec x=True in case x of {True -> False}"
>          -- LetrecM ["_x1" := ConsM (Right "True") []] (CaseM (VarM "_x1") [CAltM "True" [] (ConsM (Right "False") [])])

> t4  =  toMachineExpr "expression (\\x -> x) (\\x -> x) (\\x -> x) (\\x -> x) (\\x -> x)"
>         --  LetrecM ["_x6" := LamM "_x5" (VarM "_x5")] (AppM (LetrecM ["_x7" := LamM "_x4" (VarM "_x4")] (AppM (LetrecM ["_x8" := LamM "_x3" (VarM "_x3")] (AppM (LetrecM ["_x9" := LamM "_x2" (VarM "_x2")] (AppM (LamM "_x1" (VarM "_x1")) "_x9")) "_x8")) "_x7")) "_x6")

> t5  =  toMachineExpr "expression (seq ((\\x -> x) (\\x -> x)) (((\\x -> x) (\\x -> x)) (\\x -> x)))"
>         --  LetrecM ["_x6" := LetrecM ["_x8" := LamM "_x5" (VarM "_x5")] (AppM (LetrecM ["_x9" := LamM "_x4" (VarM "_x4")] (AppM (LamM "_x3" (VarM "_x3")) "_x9")) "_x8")] (SeqM (LetrecM ["_x7" := LamM "_x2" (VarM "_x2")] (AppM (LamM "_x1" (VarM "_x1")) "_x7")) "_x6")

> t6  =  toMachineExpr "data P = P data Q = Q (P -> P) (P -> P) expression (case Q (\\x -> x) (\\y -> y) of { (Q a b) -> (seq (a P) (b P)) })"
>         --  CaseM (LetrecM ["_x5" := LamM "_x1" (VarM "_x1"),"_x6" := LamM "_x2" (VarM "_x2")] (ConsM (Right "Q") ["_x5","_x6"])) [CAltM "Q" ["_x3","_x4"] (LetrecM ["_x7" := LetrecM ["_x9" := ConsM (Right "P") []] (AppM (VarM "_x4") "_x9")] (SeqM (LetrecM ["_x8" := ConsM (Right "P") []] (AppM (VarM "_x3") "_x8")) "_x7"))]

> t7 =  toMachineExpr "expression (\\x -> forkIO x) (return Unit)"
>        --   LetrecM ["_x2" := LetrecM ["_x4" := ConsM (Right "Unit") []] (ConsM (Left Return) ["_x4"])] (AppM (LamM "_x1" (LetrecM ["_x3" := VarM "_x1"] (ConsM (Left Fork) ["_x3"]))) "_x2")

> t8 =  toMachineExpr "expression (newMVar Unit) >>= (\\x -> takeMVar x)"
>        --  LetrecM ["_x4" := LetrecM ["_x2" := ConsM (Right "Unit") []] (ConsM (Left New) ["_x2"]),"_x5" := LamM "_x1" (LetrecM ["_ x3" := VarM "_x1"] (ConsM (Left Take) ["_x3"]))] (ConsM (Left Bind) ["_x4","_x5"])          

> t9  =  toMachineExpr "expression letrec x=x in x"
>         --  LetrecM ["_x1" := VarM "_x1"] (VarM "_x1")

> t10 =  toMachineExpr "expression (newMVar Unit) >>= (\\x -> takeMVar x)"
>         --  LetrecM ["_x4" := LetrecM ["_x2" := ConsM (Right "Unit") []] (ConsM (Left New) ["_x2"]),"_x5" := LamM "_x1" (LetrecM ["_x3" := VarM "_x1"] (ConsM (Left Take) ["_x3"]))] (ConsM (Left Bind) ["_x4","_x5"])

> t11 =  toMachineExpr "data Bool = True | False expression  letrec exch = \\mvar -> (\\content -> ((takeMVar mvar) >>= \\x0 -> (putMVar mvar content))) in ((newMVar False) >>= (\\x -> (exch x True) >>= (\\x1 -> (exch x False) >>= (\\x2 -> (exch x True) >>= (\\x3 -> (takeMVar x))))))"
>         --  LetrecM ["_x1" := LamM "_x2" (LamM "_x3" (LetrecM ["_x28" := LetrecM ["_x25" := VarM "_x2"] (ConsM (Left Take) ["_x25"]),"_x29" := LamM "_x4" (LetrecM ["_x26" := VarM "_x2","_x27" := VarM "_x3"] (ConsM (Left Put) ["_x26","_x27"]))] (ConsM (Left Bind) ["_x28","_x29"])))] (LetrecM ["_x23" := LetrecM ["_x9" := ConsM (Right "False") []] (ConsM (Left New) ["_x9"]),"_x24" := LamM "_x5" (LetrecM ["_x21" := LetrecM ["_x10" := ConsM (Right "True") []] (AppM (LetrecM ["_x11" := VarM "_x5"] (AppM (VarM "_x1") "_x11")) "_x10"),"_x22" := LamM "_x6" (LetrecM ["_x19" := LetrecM ["_x12" := ConsM (Right "False") []] (AppM (LetrecM ["_x13" := VarM "_x5"] (AppM (VarM "_x1") "_x13")) "_x12"),"_x20" := LamM "_x7" (LetrecM ["_x17" := LetrecM ["_x14" := ConsM (Right "True") []] (AppM (LetrecM ["_x15" := VarM "_x5"] (AppM (VarM "_x1") "_x15")) "_x14"),"_x18" := LamM "_x8" (LetrecM ["_x16" := VarM "_x5"] (ConsM (Left Take) ["_x16"]))] (ConsM (Left Bind) ["_x17","_x18"]))] (ConsM (Left Bind) ["_x19","_x20"]))] (ConsM (Left Bind) ["_x21","_x22"]))] (ConsM (Left Bind) ["_x23","_x24"]))

> t12 =  toMachineExpr "data Bool = True | False expression  letrec exch = \\mvar -> (\\content -> ((takeMVar mvar) >>= \\x0 -> (putMVar mvar content))) in ((newMVar False) >>= (\\x -> (exch x True) >>= (\\x1 -> (exch x False) >>= (\\x2 -> (exch x True) >>= (\\x3 -> (putMVar x True))))))"
>         --  LetrecM ["_x1" := LamM "_x2" (LamM "_x3" (LetrecM ["_x29" := LetrecM ["_x26" := VarM "_x2"] (ConsM (Left Take) ["_x26"]),"_x30" := LamM "_x4" (LetrecM ["_x27" := VarM "_x2","_x28" := VarM "_x3"] (ConsM (Left Put) ["_x27","_x28"]))] (ConsM (Left Bind) ["_x29","_x30"])))] (LetrecM ["_x24" := LetrecM ["_x9" := ConsM (Right "False") []] (ConsM (Left New) ["_x9"]),"_x25" := LamM "_x5" (LetrecM ["_x22" := LetrecM ["_x10" := ConsM (Right "True") []] (AppM (LetrecM ["_x11" := VarM "_x5"] (AppM (VarM "_x1") "_x11")) "_x10"),"_x23" := LamM "_x6" (LetrecM ["_x20" := LetrecM ["_x12" := ConsM (Right "False") []] (AppM (LetrecM ["_x13" := VarM "_x5"] (AppM (VarM "_x1") "_x13")) "_x12"),"_x21" := LamM "_x7" (LetrecM ["_x18" := LetrecM ["_x14" := ConsM (Right "True") []] (AppM (LetrecM ["_x15" := VarM "_x5"] (AppM (VarM "_x1") "_x15")) "_x14"),"_x19" := LamM "_x8" (LetrecM ["_x16" := VarM "_x5","_x17" := ConsM (Right "True") []] (ConsM (Left Put) ["_x16","_x17"]))] (ConsM (Left Bind) ["_x18","_x19"]))] (ConsM (Left Bind) ["_x20","_x21"]))] (ConsM (Left Bind) ["_x22","_x23"]))] (ConsM (Left Bind) ["_x24","_x25"]))

> expr 13 = toMachineExpr $
>  "data Bool = True | False\n" ++
>  "data ListB = ConsB Bool ListB | NilB\n" ++
>  "expression \n" ++
>  "  letrec exch = \\mvar -> (\\content -> ((takeMVar mvar) >>= \\x0 -> (putMVar mvar content)));\n" ++
>  "         cr   = \\mvar -> \\c -> forkIO (exch mvar c);\n" ++
>  "         then = \\a -> \\b -> (a >>= (\\q -> b));\n" ++
>  "         sqB  = \\mvar -> \\xs -> case xs of {NilB -> (return Unit); (ConsB y ys) -> then (cr mvar y) (sqB mvar ys)};" ++
>  "         list = (ConsB True (ConsB False (ConsB True (ConsB False NilB))))\n" ++
>  "  in  ((newMVar False) >>= (\\m -> (sqB m list) >>= (\\w -> takeMVar m)))"

> t13 = toMachineExpr $
>  "data Bool = True | False\n" ++
>  "data ListB = ConsB Bool ListB | NilB\n" ++
>  "expression \n" ++
>  "  letrec exch = \\mvar -> (\\content -> ((takeMVar mvar) >>= \\x0 -> (putMVar mvar content)));\n" ++
>  "         cr   = \\mvar -> \\c -> forkIO (exch mvar c);\n" ++
>  "         then = \\a -> \\b -> (a >>= (\\q -> b));\n" ++
>  "         sqB  = \\mvar -> \\xs -> case xs of {NilB -> (return Unit); (ConsB y ys) -> then (cr mvar y) (sqB mvar ys)};" ++
>  "         list = (ConsB True (ConsB False (ConsB True (ConsB False NilB))))\n" ++
>  "  in  ((newMVar False) >>= (\\m -> (sqB m list) >>= (\\w -> takeMVar m)))"

> -- sollte nicht deadlocken
> t14 = toMachineExpr $
>  "data Bool = True | False\n" ++
>  "data ListB = ConsB Bool ListB | NilB\n" ++
>  "expression \n" ++
>  "  letrec exch = \\mvar -> (\\content -> ((takeMVar mvar) >>= \\x0 -> (putMVar mvar content)));\n" ++
>  "         cr   = \\mvar -> \\c -> forkIO (exch mvar c);\n" ++
>  "         then = \\a -> \\b -> (a >>= (\\q -> b));\n" ++
>  "         then2 = \\a -> \\b -> (a >>= (\\q -> b));\n" ++
>  "         sqB  = \\mvar -> \\xs -> case xs of {NilB -> (return Unit); (ConsB y ys) -> then (cr mvar y) (sqB mvar ys)};" ++
>  "         list = (ConsB True (ConsB False (ConsB True (ConsB False NilB))))\n" ++
>  "  in  ((newMVar False) >>= (\\m -> (then2 (takeMVar m) (sqB m list) >>= (\\w -> (putMVar m False)))))"


> -- sollte deadlock ergeben
> t15 = toMachineExpr $
>  "data Bool = True | False\n" ++
>  "data ListB = ConsB Bool ListB | NilB\n" ++
>  "expression \n" ++
>  "  letrec exch = \\mvar -> (\\content -> ((takeMVar mvar) >>= \\x0 -> (putMVar mvar content)));\n" ++
>  "         cr   = \\mvar -> \\c -> forkIO (exch mvar c);\n" ++
>  "         then = \\a -> \\b -> (a >>= (\\q -> b));\n" ++
>  "         then2 = \\a -> \\b -> (a >>= (\\q -> b));\n" ++
>  "         sqB  = \\mvar -> \\xs -> case xs of {NilB -> (return Unit); (ConsB y ys) -> then (cr mvar y) (sqB mvar ys)};" ++
>  "         list = (ConsB True (ConsB False (ConsB True (ConsB False NilB))))\n" ++
>  "  in  ((newMVar False) >>= (\\m -> (then2 (takeMVar m) (sqB m list) >>= (\\w -> (takeMVar m)))))"

----------------------------

(CMark1Thread {name= x, control= ConsM (Left Return) [v],stack = emptyStack, ioStack = emptyStack})

> setSchedule :: CMark1State -> Int -> CMark1State
> setSchedule cm1st m = 
>   let ((n,x):l)= (queue cm1st)
>   in if n > 1 then cm1st {queue = ((n-1,x):l)} 
>      else if n==1 then cm1st {queue = l ++ [(m,x)]}
>	   		else error "CMark1-Fehler" 

> isIOVal (ConsM (Left Return) _) = True
> isIOVal _                       = False
> isVal (ConsM (Right _) _)       = True
> isVal (LamM _ _)                = True
> isVal _                         = False


=====================================================================
Die exec-Funktion
=====================================================================

> exec :: Mark1Expr -> [Mark1Var] -> [Int] -> String
> exec expr var zs = 
>   let (fState,var',zs') = finalState (startState expr) var zs
>   in  printResult fState var'  zs'

> showCons (Left a) = show a
> showCons (Right a) = a

> printResult fstate var zs = 
>  case lookupHeap "_main_" (threads fstate) of
>   Just (thread,otherthreads)  ->
>     case thread of
>      CMark1Thread {control  = VarM x}         
>       -> "<<MVARREF>>>"
>      CMark1Thread  {control = LamM _ _}       
>       ->  "<<<function>>>"
>      CMark1Thread  {control = (ConsM a args)} 
>       -> if null args then showCons a
>          else
>           let 
>            argStrings [] = []
>            argStrings (arg:xs) = 
>              let strarg = case lookupHeap arg (mvars fstate) of
>                            Just _ -> "<<<MVARREF>>>"
>                            Nothing -> let newstate   = (fstate{threads = (insertHeap "_main_" (thread{control = VarM arg}) otherthreads)})
>                                           (st,v,zs') = specialFinalState newstate var zs
>                                       in printResult st v zs'
>              in strarg:(argStrings xs)  
>           in "(" ++ showCons a ++ " " ++ concat (intersperse " " (argStrings args)) ++ ")"

spezielles finalState: 
 Der Main-Thread wird auf der Mark-1 ausgewertet, andere Threads werden auf der IO Mark 1 ausgewertet 

> specialFinalState m vars (z:zs) = 
>  let ((i,threadid):restids) = queue m -- erster Thread in der Queue
>  in 
>   if threadid == "_main_" then        -- Main-Thread ist dran
>    case lookupHeap threadid (threads m) of
>     Just (mthread,other)  -- Der Main-Thread und die restlichen Threads
>      -> if isSuccessfulMainThread (mvars m) mthread  -- Der Main-Thread ist ein Wert oder eine MVar
>          then (m,vars,zs) -- dann ist die Auswertung beendet
>          else             -- der Main-Thread muss ausgewertet werden (auf der Mark 1):
>           let -- erzeuge Zustand fuer die Mark 1:
>               mark1State = (M1.Mark1State{M1.control=control mthread, M1.stack = stack mthread, M1.heap=heap m})
>               -- werte auf der Mark 1 aus (ist durch nextStateM1 in CHF.AbsM.IOMark1 implementiert, etwas speziell, 
>               -- damit MVar-Variablen richtig behandelt werden
>               (mark1State',vars'') = IOM1.nextStateM1 (mvars m) mark1State vars
>               -- erzeuge Concurrent Mark-1 Thread aus dem Ergebnis:
>               thread' = CMark1Thread{
>                            name=threadid,
>                            control=M1.control mark1State',
>                            stack=M1.stack mark1State',
>                            ioStack=ioStack mthread}
>               -- erzeuge Concurrent Mark-1 Zustand aus dem Ergebnis:
>               m' = m{heap    = M1.heap mark1State', 
>                      threads = insertHeap threadid  thread' other}
>               -- rekursiver Aufruf (vorher das Scheduling durchfuehren)
>           in  specialFinalState (setSchedule m' z) vars'' zs 
>        -- Kein Main-Thread vorhanden: 
>     Nothing -> error "main thread not found"
>     -- Ein anderer Thread als der Main-Thread darf einen Schritt ausfuehren:
>   else specialFinalState m' vars' zs'
>  where 
>    (m',vars',zs') = nextState m vars (z:zs)

> isSuccessfulMainThread _ m@(CMark1Thread{control = ConsM (Left _) _}) =
>   isEmptyStack (stack m) && isEmptyStack (ioStack m)
> isSuccessfulMainThread _  m@(CMark1Thread{control = ConsM (Right _) _}) =
>   isEmptyStack (stack m) && isEmptyStack (ioStack m)
> isSuccessfulMainThread mv  m@(CMark1Thread{control = VarM v}) =
>   isMVar v mv && isEmptyStack (stack m) && isEmptyStack (ioStack m) 
> isSuccessfulMainThread _  m@(CMark1Thread{control = LamM _ _}) =
>   isEmptyStack (stack m) && isEmptyStack (ioStack m)
> isSuccessfulMainThread _ _ = False

> isMVar v mv = case lookupHeap  v (mv) of
>                Just _ -> True
>                _ -> False
